Description

Split the logic of UtBotSymbolicEngine into two classes:

• UtBotSymbolicEngine
• Traverser

Introduced new classes and some TODO stubs:

• StateLabel is used for marking ExecutionState accordingly to their status (INTERMIDIATE, CONCRETE, TERMINAL). See the comments in the code for more information.
• TraversalContext is a context during one Jimple instruction traversal. Now there are some TODO stubs for the future work.

Refactored several relevant places with non-functional changes:

• Changed signatures of some traversal functions
• Moved some functions to more convenient places
• Fixed hack on nullable SymbolicResult in processResult
• Other minor refactorings

Fixes #259

Details

Previously UtBotSymbolicEngine had the complex logic of different types:

• setting up everything
• working with the states queue
• Jimple travesal
• working with the symbolic state
• processing final states

The idea is to split some of the aspects of the engine logic into different classes. In this MR the extraction of Jimple traversal was done. Now we have two classes:

UtBotSymbolicEngine

Now UtBotSymbolicEngine is a manager class. It's created once for one method analysis process. We can't reuse it for different methods. It sets up everything for Traverser, controls the flow of polling states from the queue and pushing new states to the queue and also processes terminal states.

So now the next things are done in UtBotSymbolicEngine:

• setting up everything
• working with the states queue
• processing final states

Traverser

Traverser is responsible for traversing the top instruction from the passed ExecutionState. It's created inside UtBotSymbolicEngine and can't be reused between different methods ("method-under-test"s). The main function is traverse(state: ExecutionState): Collection<ExecutionState> which takes an ExecutionState and produces next states, so all other extra information needed for traversal should be passed via the constructor of Traverser.

Please note, that now it's Traverser responsibility to choose the right label for the next ExecutionState. Then UtBotSymbolicEngine matches on this label and decides what to do with this state.

So now the next things are done in Traverser:

• Jimple travesal
• working with the symbolic state

Type of Change

• Refactoring (non-functional change improving code quality)

How Has This Been Tested?

Automated Testing

Ran all tests in IDEA. No new test failures have been detected in this change.

Checklist:

• The change followed the style guidelines of the UTBot project
• Self-review of the code is passed
• The change contains enough commentaries, particularly in hard-to-understand areas
• New documentation is provided or existed one is altered
• No new warnings (Except some TODOs for the following MRs)
• All tests pass locally with my changes